Alternative Proof of Gauss Integral with improper integral#1646
Alternative Proof of Gauss Integral with improper integral#1646IshiguroYoshihiro wants to merge 1 commit intomath-comp:masterfrom
Conversation
IshiguroYoshihiro
changed the title
|
|
||
| Section u_properties. | ||
|
|
||
| Lemma integral0y_u0 : |
There was a problem hiding this comment.
The function u is internal to the module gauss_integral_proof.
It therefore seems strange to introduce a lemma integral0y_u0 that exposes the identifier u.
Maybe this new lemma should itself be inside a module.
| Section gauss_dominates. | ||
| Local Open Scope ring_scope. | ||
|
|
||
| Definition max_x : R := (Num.sqrt 2)^-1. |
There was a problem hiding this comment.
max_x looks ill-names: it talks about x which is undefined and sounds generic even though it is technical.
| (* # calculating gauss integrals by limit *) | ||
| (* ref: https://www.phys.uconn.edu/~rozman/Courses/P2400_17S/ *) | ||
| (* downloads/gaussian-integral.pdf *) | ||
| (* u (x : R) (y : R) : R == a function dominates gauss_fun over `[0, +oo[ *) |
There was a problem hiding this comment.
The function u is not really defined in this file. Maybe this piece of documentation should go to gauss_integral.v.
There was a problem hiding this comment.
And maybe the function u in gauss_integral.v could be renamed to better match its documentation. By the way, what "dominates" mean here?
|
|
||
| Let max_x_ge0 : (0 <= max_x). Proof. by rewrite invr_ge0. Qed. | ||
|
|
||
| Definition max_y : R := 2 / Num.sqrt 2 / Num.sqrt (expR 1). |
There was a problem hiding this comment.
Like max_x, may_y looks ill-named. It should also be accompanied by a piece of documentation if it is intended to be exposed. It suffices to explain its role in the proof.
3 participants
Motivation for this change
I added an alternative proof of gauss integral and placed it in theories/showcase.
This is an experimental approach of improper integral.
The difference of proof strategy is that this version mainly relies on lemmas related to integration over unbounded intervals.
[NB(rei): this is the continuation of PR #1584 ]
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Merge policy
As a rule of thumb:
all compile are preferentially merged into master.
Reminder to reviewers